Section: New Results

Type and rewriting theory

A type theory for Coq

Participants : Jean-Pierre Jouannaud, Qian Wang.

In this joint work with Bruno Barras and Pierre-Yves Strub [17] , we describe an abstract model of CoqMT [73] called CoqMTU, which puts together the Calculus of Inductive Constructions, decidable first-order theories, and an infinite hierarchy of universes which are all predicative but the first impredicative universe of propositions. We have shown its consistency, strong normalization and decidability of type checking in presence of weak elimination (and absence of strong elimination). An important feature of this work is that the first-order theory is abstract, characterized by the three natural axioms that (i) it is non-degenerated (its models have at least two elements), (ii) constructors are free, and (iii) defined symbols are completely defined. On the theoretical side, this allows us to give an abstract elimination principle for such non-canonical theories. On the practical side, this justifies the implementation of CoqMT in which decidable theories can be dynamically dowloaded. It should be noticed that these proofs are done in Coq, except for the strong normalization part. Qian Wang is now continuing this work at Ecole Polytechnique with Bruno Barras and Pierre-Yves Strub, the target being strong normalization.

Confluence by decreasing diagrams

Participants : Jean-Pierre Jouannaud, Huiying Luo, Jiaxiang Liu.

Invented by Vincent Van Oostrom, decreasing diagrams capture both kinds of diagrams arising from Newmann's Lemma and Hindley's Lemma: they indeed allow to reduce all known confluence methods to critical pairs computations, and a search of decreasing diagrams for them all, where decreasingness is measured by a well-founded order on proof steps.

In [55] , we give a new simple proof of Van Oostrom's main theorem, and extend the method of decreasing diagrams to rewrite relations on a term algebra. We prove that the union of a terminating left-linear systems, and a non-terminating linear system is confluent provided the various critical pairs existing in in their combination have decreasing diagrams (with respect to some order built from the respective orders of both systems).

During this year, we have further simplified and generalized these results in order to get rid of the left-linearity assumption for the first system, and of the right-linearity assumption for the second. This yields a true generalization of the well-known Knuth-Bendix-Huet confluence result for terminating systems, and at the same time of various critical-pair based results found in the literature for non-terminating systems.

Confluence of normal rewriting

Participants : Jean-Pierre Jouannaud, Jianqi Li.

Confluence results for first-order and higher-order rewriting differ in many ways: by the rewriting relation used, and by the strong normalization assumption made. We believe that these differences hide the strong similarities of these (and other) kinds of rewriting.

In this work, we introduce a new notion of rewriting, normal rewriting, which aims at capturing all known results reducing confluence to critical (and extension) pair computations in presence of some termination assumption.

We achieve this goal in the following way. First, we consider theories made of a set $R$ of rules, a set $S$ of simplifiers, and a set $E$ of equations. Rewriting operates on terms in $S$ modulo $E$ normal forms, and uses $S\cup E$-pattern matching for firing the rules in $R$, before to normalize the result with respect to $S$ modulo $E$. Termination is assumed for the union of $S$ modulo $E$ and $R$ modulo $S\cup E$. Second, we introduce relations on an abstract set of terms, and an abstract, well-founded set of positions, and reduce the Church-Rosser property of abstract normal rewriting to abstract notions of critical pairs and extensions. We can then apply this result to first-order rewriting, as well as to various forms of higher-order rewriting. These results capture plain rewriting ($S\cup E=\varnothing$), Stickel's rewriting modulo ($S=\varnothing$), Nipkow's higher-order reswriting ($S$ is made of beta-reduction and eta-expansion, and $E$ is alpha-conversion), and allow to describe new forms of first and higher-order rewriting relations.

Argument filterings and usable rules in higher-order rewrite systems

Participant : Frédéric Blanqui.

Joint work with Keiichirou Kusakari and Sho Suzuki from Nagoya University, Japan.

The static dependency pair method is a method for proving the termination of higher-order rewrite systems à la Nipkow [62] . It combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed lambda-calculi [52] . Argument filterings and usable rules are two important methods of the dependency pair framework used by current state-of-the-art first-order automated termination provers [51] , [53] . In [12] , we extend the class of higher-order systems on which the static dependency pair method can be applied. Then, we extend argument filterings and usable rules to higher-order rewriting, hence providing the basis for a powerful automated termination prover for higher-order rewrite systems.